Error handling cleanup in solvers/flattening #2897

danpoe · 2018-09-04T19:44:48Z

Error handling cleanup in solvers/flattening, files array.cpp to boolbv_cond.cpp (alphabetically).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 40617c9).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

tautschnig

Let's try to lift up invariants as far as possible. Several proposals below.

tautschnig · 2018-09-05T08:41:04Z

src/solvers/flattening/boolbv_add_sub.cpp


  const exprt &op0=expr.op0();
  DATA_INVARIANT(
    op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());

  bvt bv=convert_bv(op0);

-  if(bv.size()!=width)
-    throw "convert_add_sub: unexpected operand 0 width";
+  INVARIANT(


I'd say a CHECK_RETURN would do.

But really: we are doing this all the time. Couldn't we just make convert_bv take a second argument expected_width and do that check itself? This will also take the error reporting one step closer to where the error occurred, helping to fix root causes, not symptoms.

tautschnig · 2018-09-05T08:41:17Z

src/solvers/flattening/boolbv_add_sub.cpp

@@ -69,17 +76,21 @@ bvt boolbvt::convert_add_sub(const exprt &expr)

    const bvt &op=convert_bv(*it);

-    if(op.size()!=width)
-      throw "convert_add_sub: unexpected operand width";
+    INVARIANT(


CHECK_RETURN

tautschnig · 2018-09-05T08:45:24Z

src/solvers/flattening/boolbv_add_sub.cpp

+    INVARIANT(
+      op.size() == width,
+      "the width of the bitvector resulting from the expression operand should"
+      "be equal to the width indicated by the expression type");

    if(type.id()==ID_vector || type.id()==ID_complex)
    {
      const typet &subtype=ns.follow(type.subtype());

      std::size_t sub_width=boolbv_width(subtype);


While at it: remove the ns.follow in here, and let boolbv_width deal with possible symbol/tag types (just pass type.subtype() to boolbv_width.

tautschnig · 2018-09-05T08:46:12Z

src/solvers/flattening/boolbv_add_sub.cpp

@@ -91,7 +102,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)

        for(std::size_t j=0; j<tmp_op.size(); j++)
        {
-          assert(i*sub_width+j<op.size());
+          INVARIANT(
+            i * sub_width + j < op.size(), "bit index shall be within bounds");


I don't think we need to check this tmp_op.size()-times. We can just check this once before entering the loop.

The invariant is actually contained in a nested loop. It seems that the intention is also to check that we didn't mess up the index computation (e.g. by confusing i and j). How about we keep the invariant at this place and introduce a new local variable index which is set to i * sub_width + j and then use this variable in both the invariant and the array access?

Ok, that would make sense.

tautschnig · 2018-09-05T08:46:55Z

src/solvers/flattening/boolbv_add_sub.cpp

@@ -100,7 +112,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)

        for(std::size_t j=0; j<tmp_result.size(); j++)
        {
-          assert(i*sub_width+j<bv.size());
+          INVARIANT(
+            i * sub_width + j < bv.size(), "bit index shall be within bounds");


As above: check once, before entering the loop. And then consider whether it can be checked even earlier (as soon as all variables' values are known).

tautschnig · 2018-09-05T08:56:06Z

src/solvers/flattening/boolbv_complex.cpp

@@ -31,8 +34,10 @@ bvt boolbvt::convert_complex(const exprt &expr)
      {
        const bvt &tmp=convert_bv(*it);

-        if(tmp.size()!=op_width)
-          throw "convert_complex: unexpected operand width";
+        INVARIANT(


tautschnig · 2018-09-05T08:56:52Z

src/solvers/flattening/boolbv_complex.cpp

@@ -47,6 +52,8 @@ bvt boolbvt::convert_complex(const exprt &expr)

 bvt boolbvt::convert_complex_real(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_complex_real);


Could such an expression be introduced, with a proper API? I have no idea what that is, though.

It seems to be for getting the real part of a complex number. The introduction of complex_real_exprt and complex_imag_exprt has become a separate PR now: #2916.

tautschnig · 2018-09-05T08:57:10Z

src/solvers/flattening/boolbv_complex.cpp

  bv.resize(width); // chop

  return bv;
 }

 bvt boolbvt::convert_complex_imag(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_complex_imag);


As above: introduce a new complex_imag_exprt.

tautschnig · 2018-09-05T08:57:29Z

src/solvers/flattening/boolbv_concatenation.cpp

 bvt boolbvt::convert_concatenation(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_concatenation);


Use concatenation_exprt as parameter to the method.

tautschnig · 2018-09-05T08:58:45Z

src/solvers/flattening/boolbv_cond.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]

 bvt boolbvt::convert_cond(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_cond);


Introduce a cond_exprt (whatever that is).

ID_cond is never assigned to anything, I would say remove it

It seems to be a list of guarded commands, but as @romainbrenguier mentioned it's not assigned anywhere. @kroening Is this still needed or can we remove ID_cond and convert_cond?

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 40617c9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/83782391
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

chrisr-diffblue · 2018-09-14T08:46:40Z

src/solvers/flattening/boolbv.cpp

+      it->var_no() != literalt::unused_var_no(),
+      "variable number must be different from the unused variable number",
+      expr.find_source_location(),
+      expr.pretty());


Could you just pass expr to INVARIANT_WITH_DIAGNOSTICS as a structured argument rather than doing pretty() here?

Ah yes, this was done before the irep_pretty_diagnosticst PR was merged. I think I have to do this in a few more places in the other PRs as well.

danpoe · 2018-09-19T11:22:30Z

@kroening @tautschnig @peterschrammel There's two remaining questions in this PR regarding ID_case and ID_cond expressions. Both ID_case and ID_cond do not seem to be assigned anywhere. Can those cases be removed?

tautschnig · 2018-09-19T12:09:21Z

Both ID_case and ID_cond do not seem to be assigned anywhere. Can those cases be removed?

Deferring to @kroening @peterschrammel or @mgudemann: maybe EBMC has these? I don't know about the hardware stuff...

peterschrammel · 2018-09-19T12:12:29Z

They are both used in EBMC.

tautschnig · 2018-09-19T12:17:26Z

They are both used in EBMC.

Thanks. Could anyone with insight into that code base help out to provide code to go in std_expr.h?

allredj

Passed Diffblue compatibility checks (cbmc commit: 5f068f9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85324861

tautschnig

Looks good from my point of view, with some action items left.

tautschnig · 2018-09-21T13:27:26Z

src/solvers/flattening/boolbv_complex.cpp

@@ -69,7 +62,7 @@ bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr)

  bvt bv = convert_bv(expr.op());

-  assert(bv.size()==width*2);
+  INVARIANT(bv.size() == width * 2, "");


Missing message

tautschnig · 2018-09-21T13:28:18Z

src/solvers/flattening/boolbv_complex.cpp

@@ -54,7 +47,7 @@ bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)

  bvt bv = convert_bv(expr.op());

-  assert(bv.size()==width*2);
+  INVARIANT(bv.size() == width * 2, "");


Missing message, though really you should just drop it and add the extra argument to convert_bv?

allredj

Passed Diffblue compatibility checks (cbmc commit: 6d22293).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85673016

Files arrays.cpp to boolbv_cond.cpp (in alphabetical order)

allredj

Passed Diffblue compatibility checks (cbmc commit: 77e1b6c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85739351

peterschrammel · 2018-09-24T21:10:25Z

Could anyone with insight into that code base help out to provide code to go in std_expr.h?

@danpoe, could you please raise an issue with all the expressions that you would like to be added?

danpoe · 2018-09-25T09:59:27Z

Ok, raised an issue for now for the remaining expression types: #3037

danpoe requested review from kroening, martin-cs, peterschrammel and tautschnig as code owners September 4, 2018 19:44

allredj reviewed Sep 4, 2018

View reviewed changes

tautschnig requested changes Sep 5, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from 40617c9 to b9a0781 Compare September 5, 2018 16:45

danpoe requested review from pkesseli and smowton as code owners September 5, 2018 16:45

allredj reviewed Sep 6, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch 4 times, most recently from ee9241e to 4e4bbe4 Compare September 10, 2018 11:46

danpoe mentioned this pull request Sep 10, 2018

Error handling cleanup in solvers/flattening 2 #2932

Merged

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from 4e4bbe4 to 8896c52 Compare September 10, 2018 16:22

This was referenced Sep 11, 2018

Error handling cleanup in solvers/flattening 3 #2933

Merged

Error handling cleanup in solvers/flattening 4 #2934

Merged

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch 2 times, most recently from 01428ad to 4a82359 Compare September 11, 2018 17:34

danpoe mentioned this pull request Sep 12, 2018

Error handling cleanup in solvers/flattening 5 #2938

Merged

chrisr-diffblue reviewed Sep 14, 2018

View reviewed changes

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from 4a82359 to 7f58955 Compare September 19, 2018 11:17

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from 7f58955 to 5f068f9 Compare September 19, 2018 15:32

allredj reviewed Sep 19, 2018

View reviewed changes

tautschnig approved these changes Sep 21, 2018

View reviewed changes

tautschnig assigned kroening and danpoe Sep 21, 2018

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from 5f068f9 to 6d22293 Compare September 23, 2018 20:07

allredj reviewed Sep 23, 2018

View reviewed changes

Add optional expected_width parameter to convert_bv

70532f9

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from 6d22293 to af4df20 Compare September 24, 2018 13:38

Error handling cleanup in solvers/flattening

77e1b6c

Files arrays.cpp to boolbv_cond.cpp (in alphabetical order)

danpoe force-pushed the refactor/error-handling-cleanup-solvers-flattening branch from af4df20 to 77e1b6c Compare September 24, 2018 13:43

allredj reviewed Sep 24, 2018

View reviewed changes

peterschrammel approved these changes Sep 24, 2018

View reviewed changes

tautschnig merged commit f7e224b into diffblue:develop Sep 25, 2018

danpoe deleted the refactor/error-handling-cleanup-solvers-flattening branch June 2, 2020 17:13

Error handling cleanup in solvers/flattening #2897

Error handling cleanup in solvers/flattening #2897

Uh oh!

Conversation

danpoe commented Sep 4, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danpoe commented Sep 19, 2018

Uh oh!

tautschnig commented Sep 19, 2018

Uh oh!

peterschrammel commented Sep 19, 2018

Uh oh!

tautschnig commented Sep 19, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented Sep 24, 2018

Uh oh!

danpoe commented Sep 25, 2018